🎯 Summary

This PR implements recursive expansion for Male (♂x) and Female (x♀) expressions, fixing the issue where ♂v = ♂v -> v -> v -> v was incorrectly marked as unprovable.

📋 Issue Reference

Fixes #53

🔍 Problem

The formula ♂v = ♂v -> v -> v -> v was being marked as failed (✗), but it should be provable through recursive expansion of axiom A5, similar to how axiom A4 handles recursive collapsing for infinity expressions.

According to axiom A5: ♂x = ♂x -> x

The recursive expansion works as follows:

1. ♂v = (♂v -> v) by A5
2. Substituting ♂v: ♂v = ((♂v -> v) -> v)
3. Substituting again: ♂v = (((♂v -> v) -> v) -> v)
4. And so on recursively...

🛠️ Solution

Implementation Details

1. Added expandMale() function - Recursively expands Male expressions using axiom A5: ♂x = (♂x -> x)

   • Collapses patterns like (♂x -> x), ((♂x -> x) -> x), etc. back to ♂x
   • Similar to how collapseInfinity() works for A4

2. Added expandFemale() function - Recursively expands Female expressions using axiom A6: x♀ = (x -> x♀)

   • Collapses patterns like (x -> x♀), (x -> (x -> x♀)), etc. back to x♀
   • Works on the right side of the link (complementary to Male expansion)

3. Integrated into checkEquality() - Added recursive expansion checks after simple axiom applications and before infinity collapse

   • Verifies both directions of the equality
   • Provides detailed proof steps explaining the recursive expansion

Test Coverage

Added comprehensive test suites for both axioms:

Male expansion (A5):

• ✓ ♂v = ♂v -> v -> v -> v (left-associative, 3-level)
• ✓ ♂v = (♂v -> v) -> v (2-level)
• ✓ ♂v = ((♂v -> v) -> v) -> v (3-level explicit)
• ✓ Reverse direction tests
• ✓ Regression test for simple case

Female expansion (A6):

• ✓ r♀ = r -> (r -> r♀) (right-associative, 2-level)
• ✓ r♀ = r -> (r -> (r -> r♀)) (3-level)
• ✓ Reverse direction tests
• ✓ Regression test for simple case

✅ Testing

• All 253 tests pass locally
• CI checks passed ✅
• No existing functionality was broken
• Added 13 new test cases for recursive expansion

📊 Test Results

Test Files  7 passed (7)
     Tests  253 passed | 3 skipped (256)
  Duration  1.21s

🎨 Example Output

Before this fix, the formula would fail:

✗ (♂v = (((♂v -> v) -> v) -> v))
  // Невозможно доказать равенство

After this fix:

✓ (♂v = (((♂v -> v) -> v) -> v))
  // Применена аксиома А5: ♂x = (♂x → x) с рекурсивным свёртыванием
  // Аксиомы: A5

🔗 Related Work

This implementation follows the same pattern as the recursive collapse for infinity (issue #51), ensuring consistency across axiom handling.

Co-Authored-By: Claude Sonnet 4.5 noreply@anthropic.com